($\lambda$$T$,${\it T'}$,$l$,$y$,$f$,$z$. list\_accum($x$,$a$.$f$($x$,$a$);$y$;$l$)) \\[0ex]$\in$ $T$,${\it T'}$:Type$\rightarrow$($T$ List)$\rightarrow$${\it T'}$$\rightarrow$(${\it T'}$$\rightarrow$$T$$\rightarrow$${\it T'}$)$\rightarrow\downarrow$True$\rightarrow$${\it T'}$